Pierre Castéran, Jérémy Damour, Karl Palmskog, Clément Pit-Claudel, Théo Zimmermann; "Hydras & Co. Formalized mathematics in Coq for inspiration and entertainement"